
class Object {}

virtual pred Object::equals(obj: Object) {
   this = obj
}

class Dimension extends Object{
	width: Int,
	height: Int
}

virtual pred Dimension::equals(obj: Object) {
	obj.getClass[] = this.getClass[]
	this.width = obj.width
	this.height = obj.height
}

class Dimension3D extends Dimension {
	depth: Int
}

virtual pred Dimension3D.equals(obj: Object) {
	obj.getClass[] = this.getClass[]
	super.equals[obj]
	this.depth = obj.depth
}

assert equalsIsEquivalence {
	all o: Object | // reflexivity
		o.equals[o]
	all o1, o2: Object | // symmetry
		o1.equals[o2] => o2.equals[o1]
	all o1, o2, o3: Object | // transitivity
		o1.equals[o2] && o2.equals[o3] => o1.equals[o3]
}



//
// Test virtual function overloading
//

virtual pred Object::equals(x: Object, y: Object) {
   this = x
}

virtual pred Dimension::equals(x: Object, y: Object) {
	this.getClass[] = x.getClass[]
	this.width = x.width
	this.height = x.height
}


virtual pred Dimension3D.equals(x: Object, y: Object)  {
	this.getClass[] = x.getClass[]
	super.equals[x,y]
	this.depth = x.depth
}

check equalsIsEquivalence

pred SomeEquivalents {
    some disj o1,o2:Object | o1.equals[o2]
}
run SomeEquivalents for 3 but 2 int

assert noEquivalenceforDifferentTypes {
    no disj o1,o2:Object | o1.equals[o2] && o1.getClass[ ] != o2.getClass[ ]
}
check noEquivalenceforDifferentTypes




 